1. $x$ : ?Unit
\\[0ex]2. $y$ : ?Unit
\\[0ex]3. $x$ = $y$
\\[0ex]4. case $x$ of inl($x$) =$>$ $x$ $\mid$ inr($x$) =$>$ $x$ = case $y$ of inl($x$) =$>$ $x$ $\mid$ inr($x$) =$>$ $x$
\\[0ex]5. case $x$ of inl($x$) =$>$ True $\mid$ inr($x$) =$>$ False = case $y$ of inl($x$) =$>$ True $\mid$ inr($x$) =$>$ False
\\[0ex]6. $\neg$(True = False)
\\[0ex]$\vdash$  $x$ $\sim$ $y$